Nuprl Lemma : d-decl_wf
11,40
postcript
pdf
D
:Dsys,
i
:Id. d-decl(
D
;
i
)
Knd
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
d-decl(
D
;
i
)
Lemmas
w-action-dec
wf
,
ma-da
wf
,
d-m
wf
,
locl
wf
,
Id
wf
,
ma-dout
wf
,
lsrc
wf
,
IdLnk
wf
,
dsys
wf
origin
D:Dsys, i:Id. d-decl(D;i) 
Knd
Type D:Dsys, i:Id. d-decl(D;i) KndType x:A. B(x) T